$\forall$${\it es}$:ES, $m$:$\mathbb{N}^{+}$, $f$:(\{0..$m$$^{-}$\}$\rightarrow$E).
\\[0ex]($\forall$$i$:\{0..($m$ {-} 1)$^{-}$\}. ($f$($i$) $<$loc $f$($i$+1))) $\Rightarrow$ ($\forall$$i$:\{0..$m$$^{-}$\}, $j$:\{0..($i$+1)$^{-}$\}. $f$($j$) $\leq$loc $f$($i$) )